Notes (Week 9 Monday)

Very brief Hoare logic recap:


  Hoare triples

     {φ} P {ψ}

    φ precondition
    P program
    Ψ postcondition

    Reads: if φ is true in the initial state,
           then any state P can terminate in
           must satisfy ψ.

     { x contains the elements x_0,..,x_n }
       my_sorting_algorithm
     { x contains the elements x_0,..,x_n sorted in ascending order
     }

  Hoare logic:

   inference rules for proving Hoare triples

      ___________________  assign
      {φ[x:=e]} x:= e {φ}


      {φ} P {ρ}    {ρ} Q {ψ}
      _______________________  seq
         {φ} P; Q {ψ}


      {φ ∧ b} P {ψ}        {φ ∧ ¬b} Q {ψ}
      __________________________________ if
         {φ} if b then P else Q fi {ψ}


               {φ ∧ b} P {φ}
      __________________________________ while
         {φ} while b do P od {φ ∧ ¬b}


        φ ⇒ φ'    {φ'} P {ψ'}   Ψ' ⇒ Ψ
       ____________________________________ conseq
                  {φ} P {ψ}



  ⊢ {⊤} P {⊥}

  ^ it implies every other Hoare triple (about P) by the rule of consequence


  ⊢ {⊥} P {⊤}
  ^ this is the strictly most useless Hoare triple:
     it says "if you never run P, ⊤ will hold"


Two useful strats for finding loop invariants
 in this situation:

  i:=0
  m:=1
  while i < N do
    i := i + 1
    m := m × i
  od

 1: write a predicate that describes the
    current value of m

     If we can establish
        m = i!
     is a loop invariant

     Ask:
       does the postcondition follow?

       m = i! ∧ ¬i<N
       ⇒
       m = N!

       ^ no :(
         let's try to add conjuncts
         to make it work

      m = i! ∧ i ≤ N

      ^ this will work

      m = i! ∧ i ≤ N ∧ ¬N < i
      ⇒
      m = N!

 2: write a predicate that describes how
    to obtain N! from the current values
    of m and i

    (skip)


    {1 ≤ N}
    {1 = fib(1) ∧ 1 = fib(1+1) ∧ 1 ≤ N}        
    m := 1;
    {m = fib(1) ∧ 1 = fib(1+1) ∧ 1 ≤ N}
    n := 1;
    {m = fib(1) ∧ n = fib(1+1) ∧ 1 ≤ N}
    i := 1;
    {m = fib(i) ∧ n = fib(i+1) ∧ i ≤ N}
    while i < N do
      { m = fib(i) ∧ n = fib(i+1) ∧ i ≤ N ∧ i < N } *
      { n = fib(i+1) ∧ n+m = fib(i+1+1) ∧ i+1 ≤ N }
      t := m;
      { n = fib(i+1) ∧ n+t = fib(i+1+1) ∧ i+1 ≤ N }
      m := n;
      { m = fib(i+1) ∧ m+t = fib(i+1+1) ∧ i+1 ≤ N }
      n := m+t;
      { m = fib(i+1) ∧ n = fib(i+1+1) ∧ i+1 ≤ N }
      i := i+1
      { m = fib(i) ∧ n = fib(i+1) ∧ i ≤ N }
    od
    { m = fib(i) ∧ n = fib(i+1) ∧ i ≤ N ∧ ¬(i<N) }

    { m = fib(N) }


To prove the rule of consequence application at * we need to show that
   If    m = fib(i)        (1)
     and n = fib(i+1)      (2)
     and i ≤ N             (3)
     and i < N             (4)

   Then we need to prove:
      n = fib(i+1)      <-- exactly assumption (2)

      n+m = fib(i) + fib(i+1) =  (by 1,2)
          = fib(i+2) = (by definition of fib)
          = fib(i+1+1)   (cf. Russel & Whitehead)


      i+1 ≤ N   (immediate from i < N)


In assignment 1, there was an exercise where we modelled a connect 5
program as a relation between initial and final states.


The agenda:

  define a way to *systematically* compute such pre-post-state relations
  for any program in 𝓛.

    ⟦P⟧     "the semantics of P", where P ∈ 𝓛

    ⟦P⟧ ⊆ S × S        where S is the set of all states


  A Hoare triple is provable if we can derive it using the inference rules of Hoare logic

     ⊢ {φ} P {Ψ}

  Given such a semantics, we can state what it means for a Hoare triple
   to be valid:

        ⊧ {φ} P {Ψ}

        iff

        ∀s,t ∈ S. (s,t) ∈ ⟦P⟧ ∧ ⟦φ⟧s ⇒ ⟦Ψ⟧t



      ∀s,t ∈ S. (s,t) ∈ ⟦P⟧ ∧ φ(s) ⇒ Ψ(t)

Then we can state (and prove) e.g. *soundness* of Hoare logic:

  If ⊢ {φ} P {Ψ}  then ⊧ {φ} P {Ψ}

Or (TL;DR) we want to prove that Hoare logic "works", so we need to
define what "works" means ^above


   <  ⊆ ℕ × ℕ  (just bog-standard less-than on nats)

   (<); (<) =
   {(n,m) | ∃x. n < x ∧ x < m} =
   {(n,m) | n + 1 < m}

 (<)({1,2,3}) = {2,3,4,5,6,...}

 (<)({}) = {}


  ⟦b; P⟧   b a predicate, P a program

  =
  ⟦b⟧; ⟦P⟧
  =
  ⟦b⟧; ⟦P⟧
  =
  {(η,η') | ∃η''. (η,η'') ∈ ⟦b⟧ ∧ (η'',η') ∈ ⟦P⟧}
  =
  {(η,η') | ∃η''. η=η'' ∧ ⟦b⟧η = true ∧ (η'',η') ∈ ⟦P⟧}                                           

  =
  {(η,η') | ⟦b⟧η = true ∧ (η,η') ∈ ⟦P⟧}


  ⟦b⟧; ⟦P⟧ intuitively:
           the possible results of running P,
           but with b as an extra precondition


 R* is the least set defined by the following rules:


                 (x,y) ∈ R   (y,z) ∈ R*
  ___________    ____________________
  (x,x) ∈ R*         (x,z) ∈ R*


 We defined ⟦P⟧

 using three equations and one inference rule

      (η,η') ∈ ⟦x := e⟧    if   η' = η[x ↦ ⟦e⟧η]

      ⟦P; Q⟧ = ⟦P⟧; ⟦Q⟧

      ⟦if b then P else Q fi⟧ = ⟦b; P⟧ ∪ ⟦¬b; Q⟧

      ⟦while b do P od⟧ = ⟦b; P⟧*; ⟦¬b⟧